Trong phần tiếp theo, từ và đối tượng mang cùng một nghĩa; loại và hình thái mang cùng một nghĩa.

Trong một hệ hình thái, mỗi từ có một loại. Ví dụ, 4 {\displaystyle 4} , 2 + 2 {\displaystyle 2+2} và 2 ⋅ 2 {\displaystyle 2\cdot 2} là các từ phân biệt đều có loại n a t {\displaystyle \mathrm {nat} } của các số tự nhiên. Theo truyền thống, loại của từ được viết sau dấu hai chấm, chẳng hạn như 2 : n a t {\displaystyle 2:\mathrm {nat} } nghĩa là số 2 {\displaystyle 2} có loại n a t {\displaystyle \mathrm {nat} } .

Các hệ hình thái có các phép tính tường minh được thể hiện qua các luật viết lại. Các luật viết lại này được gọi là quy tắc chuyển đổi hoặc, nếu luật chỉ hoạt động theo một chiều, quy tắc rút gọn. Ví dụ, 2 + 2 {\displaystyle 2+2} và 4 {\displaystyle 4} là những từ khác nhau về mặt cú pháp, nhưng từ đầu tiên có thể được rút gọn thành từ thứ hai. Phép rút gọn này được viết là 2 + 2 ↠ 4 {\displaystyle 2+2\twoheadrightarrow 4} .

Các hàm trong hệ hình thái có một quy tắc rút gọn đặc biệt: một biến xuất hiện trong định nghĩa hàm sẽ được thay thế bởi đối số tương ứng. Giả sử hàm d o u b l e {\displaystyle \mathrm {double} } được định nghĩa là x ↦ x + x {\displaystyle x\mapsto x+x} . Phép gọi hàm d o u b l e   2 {\displaystyle \mathrm {double} \ 2} sẽ được rút gọn bằng cách thay thế 2 {\displaystyle 2} cho mọi x {\displaystyle x} trong định nghĩa hàm. Như vậy ta có phép rút gọn d o u b l e   2 ↠ 2 + 2 {\displaystyle \mathrm {double} \ 2\twoheadrightarrow 2+2} .

Loại hàm được ký hiệu bằng một mũi tên → {\displaystyle \to } từ loại tham số đến loại trả về của hàm. Như vậy, ta viết d o u b l e : n a t → n a t {\displaystyle \mathrm {double} :\mathrm {nat} \to \mathrm {nat} } (tức là, d o u b l e {\displaystyle \mathrm {double} } là một từ, loại của nó là n a t → n a t {\displaystyle \mathrm {nat} \to \mathrm {nat} } , tức là nó là một hàm lấy vào một từ của loại các số tự nhiên, và cho ra một từ của loại các số tự nhiên).